<?php

class float {}
